Nuprl Lemma : Reffect-discrete_wf
11,40
postcript
pdf
A
:es_realizer{i:l}. (
Reffect?(
A
))
(Reffect-discrete(
A
)
)
latex
Definitions
Reffect-discrete(
A
)
,
t
T
,
P
Q
,
x
:
A
.
B
(
x
)
,
prop{i:l}
Lemmas
es
realizer
wf
,
Reffect?
wf
,
assert
wf
,
bfalse
wf
,
btrue
wf
,
Reffect-f
wf
origin
A:es_realizer{i:l}. (
Reffect?(A)) 
(Reffect-discrete(A) 
) A:es_realizer{i:l}. (Reffect?(A)) (Reffect-discrete(A) ) T Qx:A. B(x)